'Weak Dependency Graph [60.0]'
------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
We have computed the following set of weak (innermost) dependency pairs:
{ r0^#(0(x1)) -> c_0(0^#(r0(x1)))
, r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
The usable rules are:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
The estimated dependency graph contains the following edges:
{r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
==> {0^#(ql(x1)) -> c_11(0^#(x1))}
{r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
==> {0^#(qr(x1)) -> c_8(0^#(x1))}
{r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
==> {1^#(ql(x1)) -> c_12(1^#(x1))}
{r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
==> {1^#(qr(x1)) -> c_9(1^#(x1))}
{r0^#(m(x1)) -> c_2(m^#(r0(x1)))}
==> {m^#(qr(x1)) -> c_10(m^#(x1))}
{r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
==> {0^#(ql(x1)) -> c_11(0^#(x1))}
{r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
==> {0^#(qr(x1)) -> c_8(0^#(x1))}
{r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
==> {1^#(ql(x1)) -> c_12(1^#(x1))}
{r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
==> {1^#(qr(x1)) -> c_9(1^#(x1))}
{r1^#(m(x1)) -> c_5(m^#(r1(x1)))}
==> {m^#(qr(x1)) -> c_10(m^#(x1))}
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
==> {0^#(ql(x1)) -> c_11(0^#(x1))}
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
==> {0^#(qr(x1)) -> c_8(0^#(x1))}
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
==> {1^#(ql(x1)) -> c_12(1^#(x1))}
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
==> {1^#(qr(x1)) -> c_9(1^#(x1))}
{0^#(qr(x1)) -> c_8(0^#(x1))}
==> {0^#(ql(x1)) -> c_11(0^#(x1))}
{0^#(qr(x1)) -> c_8(0^#(x1))}
==> {0^#(qr(x1)) -> c_8(0^#(x1))}
{1^#(qr(x1)) -> c_9(1^#(x1))}
==> {1^#(ql(x1)) -> c_12(1^#(x1))}
{1^#(qr(x1)) -> c_9(1^#(x1))}
==> {1^#(qr(x1)) -> c_9(1^#(x1))}
{m^#(qr(x1)) -> c_10(m^#(x1))}
==> {m^#(qr(x1)) -> c_10(m^#(x1))}
{0^#(ql(x1)) -> c_11(0^#(x1))}
==> {0^#(ql(x1)) -> c_11(0^#(x1))}
{0^#(ql(x1)) -> c_11(0^#(x1))}
==> {0^#(qr(x1)) -> c_8(0^#(x1))}
{1^#(ql(x1)) -> c_12(1^#(x1))}
==> {1^#(ql(x1)) -> c_12(1^#(x1))}
{1^#(ql(x1)) -> c_12(1^#(x1))}
==> {1^#(qr(x1)) -> c_9(1^#(x1))}
{b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
==> {0^#(ql(x1)) -> c_11(0^#(x1))}
{b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
==> {0^#(qr(x1)) -> c_8(0^#(x1))}
{b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
==> {1^#(ql(x1)) -> c_12(1^#(x1))}
{b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
==> {1^#(qr(x1)) -> c_9(1^#(x1))}
We consider the following path(s):
1) {b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{m(qr(x1)) -> ql(m(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
and weakly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [9]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [6]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0(b(x1)) -> qr(0(b(x1)))}
and weakly orienting the rules
{ b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0(b(x1)) -> qr(0(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [8]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{ r0(b(x1)) -> qr(0(b(x1)))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [3]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [13]
qr(x1) = [1] x1 + [2]
ql(x1) = [1] x1 + [2]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [15]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [1]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 1^#_0(7) -> 13
, 1^#_0(8) -> 13
, b^#_0(7) -> 27
, b^#_0(8) -> 27}
2) { b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [12]
qr(x1) = [1] x1 + [5]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [13]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [5]
b^#(x1) = [1] x1 + [15]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
and weakly orienting the rules
{ b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [8]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [1] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, b^#(ql(1(x1))) -> c_14(1^#(b(r1(x1))))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 1^#_0(7) -> 13
, 1^#_0(8) -> 13
, c_9_0(13) -> 13
, c_12_0(13) -> 13
, b^#_0(7) -> 27
, b^#_0(8) -> 27}
3) { r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{m(qr(x1)) -> ql(m(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{1^#(qr(x1)) -> c_9(1^#(x1))}
and weakly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [7]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [1]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
and weakly orienting the rules
{ 1^#(qr(x1)) -> c_9(1^#(x1))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [5]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
and weakly orienting the rules
{ r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, 1^#(qr(x1)) -> c_9(1^#(x1))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [2]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [8]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, 1^#(qr(x1)) -> c_9(1^#(x1))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, 1^#(qr(x1)) -> c_9(1^#(x1))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 1^#_0(7) -> 13
, 1^#_0(8) -> 13
, r1^#_0(7) -> 16
, r1^#_0(8) -> 16
, c_9_0(13) -> 13
, c_12_0(13) -> 13}
4) {b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
Details:
We apply the weight gap principle, strictly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{m(qr(x1)) -> ql(m(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
and weakly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [9]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1(b(x1)) -> qr(1(b(x1)))}
and weakly orienting the rules
{ b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1(b(x1)) -> qr(1(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0(b(x1)) -> qr(0(b(x1)))}
and weakly orienting the rules
{ r1(b(x1)) -> qr(1(b(x1)))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0(b(x1)) -> qr(0(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [2]
b(x1) = [1] x1 + [14]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [15]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(2) -> 2
, ql_0(2) -> 2
, 0^#_0(2) -> 1
, b^#_0(2) -> 1}
5) { b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [12]
qr(x1) = [1] x1 + [5]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [3]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [5]
c_13(x1) = [1] x1 + [2]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))}
and weakly orienting the rules
{ b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [8]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [1] x1 + [1]
c_13(x1) = [1] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, b^#(ql(0(x1))) -> c_13(0^#(b(r0(x1))))
, m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(2) -> 2
, ql_0(2) -> 2
, 0^#_0(2) -> 1
, c_8_0(1) -> 1
, c_11_0(1) -> 1
, b^#_0(2) -> 1}
6) { r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
and weakly orienting the rules
{ r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [2]
r0^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [7]
1^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, r0^#_0(7) -> 9
, r0^#_0(8) -> 9
, 1^#_0(7) -> 13
, 1^#_0(8) -> 13
, c_9_0(13) -> 13
, c_12_0(13) -> 13}
7) {r1^#(m(x1)) -> c_5(m^#(r1(x1)))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(m(x1)) -> c_5(m^#(r1(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [1] x1 + [1]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1^#(m(x1)) -> c_5(m^#(r1(x1)))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1^#(m(x1)) -> c_5(m^#(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0(b(x1)) -> qr(0(b(x1)))}
and weakly orienting the rules
{ r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0(b(x1)) -> qr(0(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [3]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [9]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1(b(x1)) -> qr(1(b(x1)))}
and weakly orienting the rules
{ r0(b(x1)) -> qr(0(b(x1)))
, r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1(b(x1)) -> qr(1(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [6]
0(x1) = [1] x1 + [4]
1(x1) = [1] x1 + [3]
m(x1) = [1] x1 + [2]
r1(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [13]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [1] x1 + [1]
r1^#(x1) = [1] x1 + [15]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))}
Weak Rules:
{ r1(b(x1)) -> qr(1(b(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))}
Weak Rules:
{ r1(b(x1)) -> qr(1(b(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(2) -> 2
, ql_0(2) -> 2
, m^#_0(2) -> 1
, r1^#_0(2) -> 1}
8) {r0^#(m(x1)) -> c_2(m^#(r0(x1)))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0^#(m(x1)) -> c_2(m^#(r0(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0^#(m(x1)) -> c_2(m^#(r0(x1)))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0^#(m(x1)) -> c_2(m^#(r0(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{ r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0(b(x1)) -> qr(0(b(x1)))}
and weakly orienting the rules
{ b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0(b(x1)) -> qr(0(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [1] x1 + [12]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [1]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, r0^#_0(7) -> 9
, r0^#_0(8) -> 9
, m^#_0(7) -> 15
, m^#_0(8) -> 15}
9) {r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [1]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0(b(x1)) -> qr(0(b(x1)))}
and weakly orienting the rules
{ r1^#(0(x1)) -> c_3(0^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0(b(x1)) -> qr(0(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [3]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [9]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1(b(x1)) -> qr(1(b(x1)))}
and weakly orienting the rules
{ r0(b(x1)) -> qr(0(b(x1)))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1(b(x1)) -> qr(1(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [1]
m(x1) = [1] x1 + [1]
r1(x1) = [1] x1 + [3]
b(x1) = [1] x1 + [2]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [3]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [3]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))}
Weak Rules:
{ r1(b(x1)) -> qr(1(b(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))}
Weak Rules:
{ r1(b(x1)) -> qr(1(b(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 0^#_0(7) -> 11
, 0^#_0(8) -> 11
, r1^#_0(7) -> 16
, r1^#_0(8) -> 16}
10)
{ r0^#(b(x1)) -> c_6(0^#(b(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
The usable rules for this path are the following:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [1] x1 + [2]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
and weakly orienting the rules
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [8]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [4]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [8]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [8]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [8]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, m(qr(x1)) -> ql(m(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, r0^#_0(7) -> 9
, r0^#_0(8) -> 9
, 0^#_0(7) -> 11
, 0^#_0(8) -> 11
, c_8_0(11) -> 11
, c_11_0(11) -> 11}
11)
{r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1^#(1(x1)) -> c_4(1^#(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0(b(x1)) -> qr(0(b(x1)))}
and weakly orienting the rules
{ r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0(b(x1)) -> qr(0(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [3]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [9]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1(b(x1)) -> qr(1(b(x1)))}
and weakly orienting the rules
{ r0(b(x1)) -> qr(0(b(x1)))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1(b(x1)) -> qr(1(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [1]
m(x1) = [1] x1 + [1]
r1(x1) = [1] x1 + [3]
b(x1) = [1] x1 + [2]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [3]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [1]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [8]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [1] x1 + [3]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))}
Weak Rules:
{ r1(b(x1)) -> qr(1(b(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))}
Weak Rules:
{ r1(b(x1)) -> qr(1(b(x1)))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(1(x1)) -> c_4(1^#(r1(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 1^#_0(7) -> 13
, 1^#_0(8) -> 13
, r1^#_0(7) -> 16
, r1^#_0(8) -> 16}
12)
{ r1^#(b(x1)) -> c_7(1^#(b(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
The usable rules for this path are the following:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [2]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [1]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
and weakly orienting the rules
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [8]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [4]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [8]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [8]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [1] x1 + [8]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [1] x1 + [1]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 1^#(ql(x1)) -> c_12(1^#(x1))
, m(qr(x1)) -> ql(m(x1))
, 1^#(qr(x1)) -> c_9(1^#(x1))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 1^#_0(7) -> 13
, 1^#_0(8) -> 13
, r1^#_0(7) -> 16
, r1^#_0(8) -> 16
, c_9_0(13) -> 13
, c_12_0(13) -> 13}
13)
{ r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, m^#(qr(x1)) -> c_10(m^#(x1))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, m^#(qr(x1)) -> c_10(m^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [1]
m^#(x1) = [1] x1 + [3]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0^#(m(x1)) -> c_2(m^#(r0(x1)))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0^#(m(x1)) -> c_2(m^#(r0(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [1] x1 + [9]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [1] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
Weak Rules:
{ r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
Weak Rules:
{ r0^#(m(x1)) -> c_2(m^#(r0(x1)))
, m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, r0^#_0(7) -> 9
, r0^#_0(8) -> 9
, m^#_0(7) -> 15
, m^#_0(8) -> 15
, c_10_0(15) -> 15}
14)
{ r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, m^#(qr(x1)) -> c_10(m^#(x1))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, m^#(qr(x1)) -> c_10(m^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [3]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [1] x1 + [3]
r1^#(x1) = [1] x1 + [1]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [1]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1^#(m(x1)) -> c_5(m^#(r1(x1)))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1^#(m(x1)) -> c_5(m^#(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [1] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [1] x1 + [1]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
Weak Rules:
{ r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
Weak Rules:
{ r1^#(m(x1)) -> c_5(m^#(r1(x1)))
, m(qr(x1)) -> ql(m(x1))
, m^#(qr(x1)) -> c_10(m^#(x1))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, m^#_0(7) -> 15
, m^#_0(8) -> 15
, r1^#_0(7) -> 16
, r1^#_0(8) -> 16
, c_10_0(15) -> 15}
15)
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
The usable rules for this path are the following:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{m(qr(x1)) -> ql(m(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [11]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [1] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
and weakly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0^#(b(x1)) -> c_6(0^#(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [1] x1 + [8]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{ r0^#(b(x1)) -> c_6(0^#(b(x1)))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [4]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [4]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [1] x1 + [1]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(b(x1)) -> c_6(0^#(b(x1)))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, r0^#_0(7) -> 9
, r0^#_0(8) -> 9
, 0^#_0(7) -> 11
, 0^#_0(8) -> 11}
16)
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
The usable rules for this path are the following:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, m(qr(x1)) -> ql(m(x1))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{m(qr(x1)) -> ql(m(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [11]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
and weakly orienting the rules
{m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r1^#(b(x1)) -> c_7(1^#(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [1]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [8]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{ r1^#(b(x1)) -> c_7(1^#(b(x1)))
, m(qr(x1)) -> ql(m(x1))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [4]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [4]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [5]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [1] x1 + [1]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r1^#(b(x1)) -> c_7(1^#(b(x1)))
, m(qr(x1)) -> ql(m(x1))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 1^#_0(7) -> 13
, 1^#_0(8) -> 13
, r1^#_0(7) -> 16
, r1^#_0(8) -> 16}
17)
{r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0^#(1(x1)) -> c_1(1^#(r0(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [1] x1 + [5]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{ r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [8]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [8]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [1]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [0] x1 + [0]
c_1(x1) = [1] x1 + [0]
1^#(x1) = [1] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(1(x1)) -> c_1(1^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(2) -> 2
, ql_0(2) -> 2
, r0^#_0(2) -> 1
, 1^#_0(2) -> 1}
18)
{r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [4]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [4]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [1]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
and weakly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [8]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [1] x1 + [5]
c_0(x1) = [1] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
and weakly orienting the rules
{ r0^#(0(x1)) -> c_0(0^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [15]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [8]
qr(x1) = [1] x1 + [0]
ql(x1) = [1] x1 + [8]
r0^#(x1) = [1] x1 + [1]
c_0(x1) = [1] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [0] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [0] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))}
Weak Rules:
{ r0(b(x1)) -> qr(0(b(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, r1(b(x1)) -> qr(1(b(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, r0^#_0(7) -> 9
, r0^#_0(8) -> 9
, 0^#_0(7) -> 11
, 0^#_0(8) -> 11}
19)
{ r0^#(0(x1)) -> c_0(0^#(r0(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
The usable rules for this path are the following:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [1] x1 + [3]
c_0(x1) = [1] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [9]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [1]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [0]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [2]
r0^#(x1) = [1] x1 + [9]
c_0(x1) = [1] x1 + [7]
0^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [0] x1 + [0]
c_3(x1) = [0] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, m(qr(x1)) -> ql(m(x1))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, m(qr(x1)) -> ql(m(x1))
, r0^#(0(x1)) -> c_0(0^#(r0(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, r0^#_0(7) -> 9
, r0^#_0(8) -> 9
, 0^#_0(7) -> 11
, 0^#_0(8) -> 11
, c_8_0(11) -> 11
, c_11_0(11) -> 11}
20)
{ r1^#(0(x1)) -> c_3(0^#(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
The usable rules for this path are the following:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
We have applied the subprocessor on the union of usable rules and weak (innermost) dependency pairs.
'Weight Gap Principle'
----------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, m(qr(x1)) -> ql(m(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
We apply the weight gap principle, strictly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
and weakly orienting the rules
{}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ m(qr(x1)) -> ql(m(x1))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [1]
ql(x1) = [1] x1 + [0]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [0]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [3]
c_3(x1) = [1] x1 + [0]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [1]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [1]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
We apply the weight gap principle, strictly orienting the rules
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
and weakly orienting the rules
{ m(qr(x1)) -> ql(m(x1))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
using the following strongly linear interpretation:
Processor 'Matrix Interpretation' oriented the following rules strictly:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))}
Details:
Interpretation Functions:
r0(x1) = [1] x1 + [0]
0(x1) = [1] x1 + [0]
1(x1) = [1] x1 + [0]
m(x1) = [1] x1 + [0]
r1(x1) = [1] x1 + [1]
b(x1) = [1] x1 + [0]
qr(x1) = [1] x1 + [9]
ql(x1) = [1] x1 + [2]
r0^#(x1) = [0] x1 + [0]
c_0(x1) = [0] x1 + [0]
0^#(x1) = [1] x1 + [1]
c_1(x1) = [0] x1 + [0]
1^#(x1) = [0] x1 + [0]
c_2(x1) = [0] x1 + [0]
m^#(x1) = [0] x1 + [0]
r1^#(x1) = [1] x1 + [9]
c_3(x1) = [1] x1 + [7]
c_4(x1) = [0] x1 + [0]
c_5(x1) = [0] x1 + [0]
c_6(x1) = [0] x1 + [0]
c_7(x1) = [0] x1 + [0]
c_8(x1) = [1] x1 + [0]
c_9(x1) = [0] x1 + [0]
c_10(x1) = [0] x1 + [0]
c_11(x1) = [1] x1 + [0]
c_12(x1) = [0] x1 + [0]
b^#(x1) = [0] x1 + [0]
c_13(x1) = [0] x1 + [0]
c_14(x1) = [0] x1 + [0]
Finally we apply the subprocessor
'fastest of 'combine', 'Bounds with default enrichment', 'Bounds with default enrichment''
------------------------------------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, m(qr(x1)) -> ql(m(x1))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
Details:
The problem was solved by processor 'Bounds with default enrichment':
'Bounds with default enrichment'
--------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost relative runtime-complexity with respect to
Strict Rules:
{ r1(0(x1)) -> 0(r1(x1))
, r1(1(x1)) -> 1(r1(x1))
, r1(m(x1)) -> m(r1(x1))
, r1(b(x1)) -> qr(1(b(x1)))
, 0(qr(x1)) -> qr(0(x1))
, 1(qr(x1)) -> qr(1(x1))
, 0(ql(x1)) -> ql(0(x1))
, 1(ql(x1)) -> ql(1(x1))
, r0(0(x1)) -> 0(r0(x1))
, r0(1(x1)) -> 1(r0(x1))
, r0(m(x1)) -> m(r0(x1))
, r0(b(x1)) -> qr(0(b(x1)))}
Weak Rules:
{ b(ql(0(x1))) -> 0(b(r0(x1)))
, b(ql(1(x1))) -> 1(b(r1(x1)))
, 0^#(ql(x1)) -> c_11(0^#(x1))
, 0^#(qr(x1)) -> c_8(0^#(x1))
, m(qr(x1)) -> ql(m(x1))
, r1^#(0(x1)) -> c_3(0^#(r1(x1)))}
Details:
The problem is Match-bounded by 0.
The enriched problem is compatible with the following automaton:
{ qr_0(7) -> 7
, qr_0(8) -> 7
, ql_0(7) -> 8
, ql_0(8) -> 8
, 0^#_0(7) -> 11
, 0^#_0(8) -> 11
, r1^#_0(7) -> 16
, r1^#_0(8) -> 16
, c_8_0(11) -> 11
, c_11_0(11) -> 11}